(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #x7e66246e80ab6b7b) #x8199db917f549485))
(constraint (= (f #xe6e7e52716ee5abe) #x19181ad8e911a541))
(constraint (= (f #x889ee15547ec25dd) #x0000000000000001))
(constraint (= (f #x4d9e112350516e09) #x0000000000000001))
(constraint (= (f #x8ee3171dcec151a9) #x0000000000000001))
(constraint (= (f #xa63a4be6533d9767) #x59c5b419acc26899))
(constraint (= (f #x52c0e1990a739a55) #x0000000000000001))
(constraint (= (f #x0d8474ed033c2c98) #x0000000000000000))
(constraint (= (f #x263e4e5ada70ec54) #x0000000000000000))
(constraint (= (f #x94319e6ddc6d8c06) #x6bce6192239273f9))
(constraint (= (f #xe82106de11715507) #x17def921ee8eaaf9))
(constraint (= (f #xd6556a69ae3e7e3c) #x0000000000000000))
(constraint (= (f #x8da1679d925651d0) #x0000000000000000))
(constraint (= (f #x165504a6534a5043) #xe9aafb59acb5afbd))
(constraint (= (f #x032ea2ae7475277c) #x0000000000000000))
(constraint (= (f #xdeb3e6557ee831c9) #x0000000000000001))
(constraint (= (f #xe39d337676eebb19) #x0000000000000001))
(constraint (= (f #xe55b416eda5b0ae0) #x0000000000000000))
(constraint (= (f #x1b0380162e0eecb0) #x0000000000000000))
(constraint (= (f #x42d4130b34c0aee5) #x0000000000000001))
(constraint (= (f #x4e3eec2703eac136) #xb1c113d8fc153ec9))
(constraint (= (f #x6d2692e12942ecab) #x92d96d1ed6bd1355))
(constraint (= (f #xe2a5e38c537e7eaa) #x1d5a1c73ac818155))
(constraint (= (f #x6a5275b6a7999b0a) #x95ad8a49586664f5))
(constraint (= (f #xe27eaeb1ee6ddd8a) #x1d81514e11922275))
(constraint (= (f #x1ec3042e87c14536) #xe13cfbd1783ebac9))
(constraint (= (f #x434b1da2261a8c4e) #xbcb4e25dd9e573b1))
(constraint (= (f #x8945cd5d9b848583) #x76ba32a2647b7a7d))
(constraint (= (f #xbd710e1a6c8bec4a) #x428ef1e5937413b5))
(constraint (= (f #xa95b567535e106c9) #x0000000000000001))
(constraint (= (f #x722913c1965e2dbc) #x0000000000000000))
(constraint (= (f #x81bb175d8ec2525e) #x7e44e8a2713dada1))
(constraint (= (f #xde6eeb9ee31e7ce9) #x0000000000000001))
(constraint (= (f #xaa343489b0b59d08) #x0000000000000000))
(constraint (= (f #x04167490980ced4d) #x0000000000000001))
(constraint (= (f #x806e12969555b7e6) #x7f91ed696aaa4819))
(constraint (= (f #x1697eee32e17149d) #x0000000000000001))
(constraint (= (f #xc49e3419ad1546b3) #x3b61cbe652eab94d))
(constraint (= (f #xea6b3deb9e993dc0) #x0000000000000000))
(constraint (= (f #xbed072e387114c7d) #x0000000000000001))
(constraint (= (f #xc68ab0469c7934d8) #x0000000000000000))
(constraint (= (f #x354e3bed26a139c7) #xcab1c412d95ec639))
(constraint (= (f #x8818e0e094e90b12) #x77e71f1f6b16f4ed))
(constraint (= (f #x101830e1b3962b4c) #x0000000000000000))
(constraint (= (f #x11e6a71ccc095a16) #xee1958e333f6a5e9))
(constraint (= (f #xd50a444c60934ded) #x0000000000000001))
(constraint (= (f #x71d84d3c680534e4) #x0000000000000000))
(constraint (= (f #x5566c3182b1e8e38) #x0000000000000000))
(constraint (= (f #x552ce587274052eb) #xaad31a78d8bfad15))
(constraint (= (f #x4ed803aee1965e30) #x0000000000000000))
(constraint (= (f #xe1443615c7770d17) #x1ebbc9ea3888f2e9))
(constraint (= (f #xc1a5632ee1db6c11) #x0000000000000001))
(constraint (= (f #x3de238a0e2b9d316) #xc21dc75f1d462ce9))
(constraint (= (f #xaebe5d0624bd3173) #x5141a2f9db42ce8d))
(constraint (= (f #xdb0ae8c600a10eec) #x0000000000000000))
(constraint (= (f #x9ee389c90ae504c9) #x0000000000000001))
(constraint (= (f #x206aee8e1715c2d5) #x0000000000000001))
(constraint (= (f #x4535ecbac1e76a91) #x0000000000000001))
(constraint (= (f #x60c95896733e621e) #x9f36a7698cc19de1))
(constraint (= (f #x75da1230a625e326) #x8a25edcf59da1cd9))
(constraint (= (f #xe58e375e5300a7b7) #x1a71c8a1acff5849))
(constraint (= (f #xeaeed5e8a7969b4d) #x0000000000000001))
(constraint (= (f #xb27072b801bd52e1) #x0000000000000001))
(constraint (= (f #xb3ec8e8205498d73) #x4c13717dfab6728d))
(constraint (= (f #xb7a275e6eaea116e) #x485d8a191515ee91))
(constraint (= (f #xa484c37690cd6343) #x5b7b3c896f329cbd))
(constraint (= (f #x1147ae74e24d83e5) #x0000000000000001))
(constraint (= (f #x6b8e03dc506a952e) #x9471fc23af956ad1))
(constraint (= (f #x071589abb1ec6428) #x0000000000000000))
(constraint (= (f #x3acd197b4ad0317d) #x0000000000000001))
(constraint (= (f #x6c76ae0266a554d4) #x0000000000000000))
(constraint (= (f #x9bde2693a0b429cd) #x0000000000000001))
(constraint (= (f #xaaa313ad165ed060) #x0000000000000000))
(constraint (= (f #x58ee7d991b81ebe3) #xa7118266e47e141d))
(constraint (= (f #x850e22838e1685da) #x7af1dd7c71e97a25))
(constraint (= (f #xed885c3ac79ce79a) #x1277a3c538631865))
(constraint (= (f #xc471badae8d8eb5d) #x0000000000000001))
(constraint (= (f #x68e6002eeb165ba1) #x0000000000000001))
(constraint (= (f #xcb82b3b482c58c5b) #x347d4c4b7d3a73a5))
(constraint (= (f #x90c202ae7e95c311) #x0000000000000001))
(constraint (= (f #x02ae8dea6921dbc0) #x0000000000000000))
(constraint (= (f #x6e7d50635c0309e1) #x0000000000000001))
(constraint (= (f #xc357ae6ee55eee93) #x3ca851911aa1116d))
(constraint (= (f #x6ad536a4e4b6e80e) #x952ac95b1b4917f1))
(constraint (= (f #xeeaa1214c454bec0) #x0000000000000000))
(constraint (= (f #xab2488a6679d7ceb) #x54db775998628315))
(constraint (= (f #x63ea7d0bb9bb3802) #x9c1582f44644c7fd))
(constraint (= (f #xd6559db6d09aecc2) #x29aa62492f65133d))
(constraint (= (f #x775c9e58d29edbec) #x0000000000000000))
(constraint (= (f #x4e456b694ebe45c3) #xb1ba9496b141ba3d))
(constraint (= (f #x8851a72ba35be26e) #x77ae58d45ca41d91))
(constraint (= (f #xb96dd6024d555d43) #x469229fdb2aaa2bd))
(constraint (= (f #xe4740c56cc63e2bc) #x0000000000000000))
(constraint (= (f #xc6423ad85161c0ac) #x0000000000000000))
(constraint (= (f #xdc7d3c6ebe73473b) #x2382c391418cb8c5))
(constraint (= (f #xa3349405ea79813e) #x5ccb6bfa15867ec1))
(constraint (= (f #xee8596ad7ee4386e) #x117a6952811bc791))
(constraint (= (f #xe51b68953e81eb1e) #x1ae4976ac17e14e1))
(constraint (= (f #x9e54193ee07ac133) #x61abe6c11f853ecd))
(constraint (= (f #x25a6a2a9460ea10c) #x0000000000000000))
(check-synth)
(define-fun f_1 ((x (BitVec 64))) (BitVec 64) (ite (= (bvor #x0000000000000001 x) x) (ite (= (bvor #x0000000000000002 x) x) (bvneg x) #x0000000000000001) (ite (= (bvor #x0000000000000002 x) x) (bvnot x) #x0000000000000000)))
